\documentclass[compress,brown]{beamer}

\usepackage{hyperref}
\usepackage[english]{babel}
\usepackage[utf8]{inputenc}

% AMSLATEX packages
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{amsfonts}

\usepackage[]{listings}
%\usepackage{beamerthemesplit}
\usetheme{Warsaw}

\hypersetup{%
	pdftitle={Solving Satisfiable Constraints over Finite Domains},%
	pdfauthor={Thomas Hofer},%
	pdfsubject={LARA},%
	pdfkeywords={LaTeX,beamer,slides,DPLL,constraints,finite domains}%
}

\title{Solving Satisfiable Constraints over Finite Domains}
\author{Thomas Hofer}
\date{May 29th, 2008}
\institute{
	\inst{}EPFL --
	SAV'08
}


\input{listingsScala}

\begin{document}
\lstset{language=scala, columns=fullflexible,showstringspaces=false,mathescape=true}

\frame{\titlepage}

\frame[shrink=.5]{\frametitle{Outline}\tableofcontents}

\section{Introduction}

\subsection{Constraint Satisfaction Problems}

\frame{\frametitle{Examples}
	\begin{itemize}
		\item<1-> Eight queens problem
		\item<2-> Four color theorem
		\item<3-> Sudoku
		\item<4-> Linear programs
		\item<5-> SAT
		\item<6-> Contracts verification
	\end{itemize}
}

\frame{\frametitle{Definitions}
	The usual input to a CSP is a triple $\langle X, D, C\rangle$, where $X$ is a set of
	variables, $D$ a domain of values and $C$ a set of constraints.\\
	\pause
	In turn, constraints consist of a tuple of variables and a relation over
	$D^n$.\\
	\pause
	An evaluation of the variables is a function $v: X \rightarrow D$, which maps
	variables to values.\\
	\pause
	An evaluation satisfies a constraint $\langle (x_1,\ldots,x_n),R \rangle$ iff
	$(v(x_1),\ldots,v(x_n)) \in R$.\\
	\pause
	A solution to a CSP instance is an evaluation that satisfies all constraints.
}

	\frame{\frametitle{Usual algorithms}
		\begin{itemize}
			\item<1-> Simplex
			\item<2-> Backtracking
			\item<3-> Backmarking
			\item<4-> Backjumping
			\item<5-> Constraint learning
			\item<6-> Constraint propagation
			\item<7-> DPLL...
		\end{itemize}
	}

	\frame{\frametitle{Complexity}
		Constraint Satisfaction Problems range from very simple to extremely
		hard...\\

		Some of them can be solved in polynomial time, while others are known to be
		NP-complete.
}

\section{Solving Satisfiable Constraints over Finite Domains}

%\subsection{FDCSP}

%\frame{\frametitle{Relaxation of definitions}
%	In Finite Domains Constraint Statisfaction Problems, each variable can be
%	mapped to its own domain: there isn't one single domain anymore...\\
%	\pause
%	The input to such a problem is therefore something like: $\langle \overline{X}:
%	\overline{D}, C\rangle$. Where $\overline{X}: \overline{D}$ denotes a vector
%	of $x_i: D_i$, meaning that $x_i$ takes its values from domain $D_i$.\\
%	\pause
%	Hence, the complexity is significantly increased.
%}

\subsection{Our Finite Domain}

\frame{\frametitle{A Functional Scala Subset}
	\begin{itemize}
		\item $P := \{D\}\ \{E\}\ E$
		\item $D :=\ 'def\ name: T = E$
		\item $E :=\ '\{\ {E}\ '\}\ |\ F\ |\ val\ name\ =\ E$ 
		\item $F := E\ binOp\ E\ |\ !E$
		\item $T := type$
	\end{itemize}
}

\frame{\frametitle{Constraints}
	\begin{itemize}
		\item $C := C\lor C\ |\ !C\ |\ V=V$
		\item $V := ground terms$
	\end{itemize}
}

\subsection{Solving CPS}

\begin{frame}[fragile]
\frametitle{Adapted DPLL}
\begin{lstlisting}
def DPLL(S : Set[Constraint]) : Option[Evaluation] =
  val S' = RemoveSubsumed(PropagateConstraint(S))
  if (contradiction in S') then None
  else if (S' isOK) then Some(...)
  else
		val P = pick variable from FV(S')
		branch(S', P)
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Branching}
	Many branching heuristics exist and could be implemented.
\end{frame}

\section{Conclusion}

\frame{\frametitle{Remaining work}
	\begin{itemize}
		\item Constraint unification
		\item Implement an compare different branching heuristics
	\end{itemize}
}

\frame{
	\frametitle{Questions ?}
}
\end{document}
